/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.winningCondition;

import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatManager.SymbTableFactory;
import chameleon.model.NuGatStructure.prop.PropDbGame;
import chameleon.model.formula.Formula;
import chameleon.model.formula.parser.BooleanParser;
import chameleon.model.formula.parser.LtlParser;
import java.io.IOException;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 * This class create a winning condition on base of a the paramater of the following
 * commands:
 *      -compute_pre_image
 *      -compute_strategy
 * 
 * @author simon
 */
public class WinningConditionFactory {
    
    public WinningConditionFactory(){;}
    
    
    //******************* CONSTRUCTION OF A WINNING CONDITION ****************//
    
    public WinningCondition constructWinningCondition(NuGatInterface nugat,
            String[] param, PropDbGame propDbGame){
        
        //First description by an ltl formula or an smv format
        if (param[1].equals("st") )
            return constructSmvCondition(nugat,param,propDbGame);
        else if(param[1].equals("lt") && param.length==4)
            return constructLtlCondition(nugat,param,propDbGame);
        else
            throw new RuntimeException("Error during the construction of the winning"
                    + "condition, please give one of the following paramater :\n"
                    + "  -st\n"
                    + "  -lt");
    }

    private WinningCondition constructSmvCondition(NuGatInterface nugat, String[] param,
            PropDbGame propDbGame) {
        /**
         * Here we have the following informationq : 
         *  -player
         *  -property type
         *  -condition
         */
        WinningCondition condition;
        condition = new WinningCondition(nugat);
        
        condition.setProperty(param[2]);
        condition.setPlayer(param[3]);
        
        //Add the smv map table
        
        SymbTableFactory factory = new SymbTableFactory(propDbGame, nugat);
        condition.setSmvTable(factory.createSymboleTable(null));
        
        if (condition.getPropertyKind() == Tag.AVOIDTARGET ||
                condition.getPropertyKind() == Tag.REACHTARGET){
            BooleanParser parser = new BooleanParser(param[4]);
            try {
                condition.setExpOpt(parser.createFormula());
            } catch (IOException ex) {
                Logger.getLogger(WinningConditionFactory.class.getName()).log(Level.SEVERE, null, ex);
            }
        }
        else if (condition.getPropertyKind() == Tag.GENREACTIVITY){
            condition.setGRleft(param[4]);
            condition.setGRRight(param[5]);
        }
        else if (condition.getPropertyKind() == Tag.BUCHIGAME)
            condition.setGRleft(param[4]);
        else if (condition.getPropertyKind() == Tag.LTLGAME){
            try {
                LtlParser parser = new LtlParser(param[4]);
                condition.setExpOpt(parser.createFormula());
            } catch (IOException ex) {
                Logger.getLogger(WinningConditionFactory.class.getName()).log(Level.SEVERE, null, ex);
            } 
        }
        
        return condition;
    }

    private WinningCondition constructLtlCondition(NuGatInterface nugat, String[] param, PropDbGame propDbGame) {
        WinningCondition condition = null;
        try {
            SymbTableFactory factory = new SymbTableFactory(propDbGame,nugat);
            LtlParser parser = new LtlParser(param[3]);
            Formula formula = parser.createFormula();
            condition = new WinningCondition(nugat, formula, param[2],
                    factory.createSymboleTable(null));
        } catch (IOException ex) {
            Logger.getLogger(WinningConditionFactory.class.getName()).log(Level.SEVERE, null, ex);
        }
        
            
        return condition;
    }
    
}
